T:Type{i}, L:(T List), P:({x:T| (x  L)} {x:T| (x  L)} {i'}).
no_repeats(T;L)  (x, y:{x:T| (x  L)} . ((x = y))  P(x,y))  (x,yL.  P(x,y)) 

latex

Definitions	no_repeats(T;l), (x,yL.  P(x;y)), Type, t  T, type List, , x:AB(x), (x  l), {x:A| B(x)} , x:A. B(x), f(a), x(s1,s2), s = t, A, P  Q, i  j , ||as||, {i..j}, False, P & Q, A  B, i  j < k, , l[i], #$n,
Lemmas	le wf, length wf1, list-set-type, select wf, not wf, no repeats wf, l member wf